ma-single-sends0(B;T;a;l;tg;f)
== with declarations 
== ds:
== da:a : B  rcv(l,tg) : T
== a(v) sends [<tg,s,v. f(v)>] s v on link l 

latex

---

clarification:

ma-single-sends0(B;T;a;l;tg;f)
== with declarations 
== ds:
== da:fpf-join(KindDeq;a : B;rcv(l,tg) : T)
== a(v) sends <tg,s,v. f(v)>.nil s v on link l 

latex

Definitions	with declarations ds:dsda:dak(v) sends f s v on link l, , f  g, KindDeq, x : v, rcv(l,tg), car.cdr, <a,b>, x.A(x), f(a), nil
FDL editor aliases	ma-single-sends0